A main reason for unexpected delays and additional costs are errors in the design phase of digital circuits. To avoid these, various simulation procedures are currently used for verifying a logical circuit design. Unfortunately, the number of simulations needed for verifying a circuit or a data-processing system grows exponentially with the number of inputs of combinatorial circuits and even faster for sequential circuits since all possible input sequences must be simulated in these. Although such methods for simulating digital circuits are widely used and have an important place in the design process of such circuits, they are far from suitable for completely checking and verifying circuits which is why the correctness of a circuit, that is to say the correspondence between its actual implementation and its design specification cannot be guaranteed. For this reason, formal verification methods must be preferred to any type of simulation since, in principle, these can prove the complete correctness of a circuit.
Specifications of combinatorial or synchronous sequential circuits are frequently formulated in the form of so-called hardware description languages (HDL). In these cases, formal verification means the comparison of a digital circuit such as is given, for example, in the form of a network list, with its specification in the form of a description, using the methods of a hardware description language. From the literature (Erik Tiden, Richard Schmid, "Verifying ASICs in symbolic simulation", in EURO ASIC 90, 1990), formal circuit verification tools are known, the applicability of which, however, is restricted to combinatorial circuits. The formal verification of sequential digital circuits is much more difficult and only a few approaches to a solution to the problem of verifying digital circuits with a large number of states are known.